COMMENT ⊗   VALID 00003 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	.<<priori[s84,jmc]		Prioritized circumscription>>
C00008 00003	Namely we define %2ab_<_ab'%1 by
C00009 ENDMK
C⊗;
.<<priori[s84,jmc]		Prioritized circumscription>>

#. %3Prioritized circumscription%1

	An alternate way of introducing circumscription is by means of an
ordering on tuples of predicates satisfying an axiom.  We define
%2P_≤_P'%1 by

!!k10:	%2∀P P'.P ≤ P' ≡ ∀x.E(P,x) ⊃ E(P',x)%1.

That ⊗P0 is a relative minimum in this ordering is expressed by

!!k11:	%2∀P.P ≤ P0 ⊃ P = P0%1,

where equality is interpreted extensionally, i.e. we have

!!k12:	%2∀P P'.P = P' ≡ (∀x.P x ≡ P' x)%1.

Assuming that we look for a minimum among predicates ⊗P satisfying
⊗A(P), then ({eq k10}) expands to precisely to the circumscription
formula ({eq a1}).  In some earlier expositions of circumscription
this ordering approach was used, and Vladimir Lifschitz (1984)
has recently advocated
returning to it as a more fundamental and understandable concept.

	I'm beginning to think he's right about it being more
understandable, but there seems to be a more fundamental reason
for using it.  Namely, certain common sense axiomatizations are
easier to formalize if we use ordering, and these orderings don't
seem to reduce to the ordinary formula circumscription.

	%2We call it %3prioritized circumscription%1.

	Suppose we write some bird axioms in the form

!!k1:	%2∀x.¬ab aspect1 x ⊃ ¬flies x%1

and

!!k2:	%2∀x.bird x ∧ ¬ab aspect2 x ⊃ ab aspect1 x%1.

	The intent is clear.  The goal is that being a bird and
not abnormal in ⊗aspect2 prevents
the application of ({eq k1}).  However, circumscribing ⊗ab with
the axioms as written doesn't have this effect.  Namely, ({eq k2})
is equivalent to

!!k3:	%2∀x.bird x ⊃ ab aspect1 x ∨ ab aspect2 x%1,

and there is no indication that one would prefer to have
⊗aspect1_x abnormal than to have ⊗aspect2_x abnormal.  This is
why the axioms were written as they are in section 4.

	However, by using the ordering we can leave ({eq k1}) and
({eq k2}) as is, and still get the desired effect.

	We define two orderings on ⊗ab predicates, namely

!!k4:	%2∀ab ab'.ab ≤q1 ab' ≡ ∀x.ab aspect1 x ⊃ ab' aspect1 x%1

and

!!k5:	%2∀ab ab'.ab ≤q2 ab' ≡ ∀x.ab aspect2 x ⊃ ab' aspect2 x%1.

We then combine these orderings lexicographically giving %2≤q2%1
priority over %2≤q1%1 getting

!!k6:	%2∀ab ab'.ab ≤%41<2%* ab' ≡ ab ≤q2 ab' ∨ ab =q2 ab' ∧ ab ≤q1 ab'%1.

	Choosing ⊗ab0 so as to minimize this ordering yields the
result that exactly birds can fly.  However, if we add

!!k7:	%2∀x.ostrich x ⊃ ab aspect2 x%1,

we'll get that ostriches (whether or not ostriches are birds)
don't fly without further axioms.  If we use

!!k8:	%2∀x.ostrich x ∧ ¬ab aspect3 x ⊃ ab aspect2 x%1

instead of ({eq k7}), we'll have to revise our notion of ordering
to put minimizing %2ab_aspect3_x%1 at higher priority than minimizing
⊗aspect2_x and %2a fortiori%1 at higher priority than minimizing
⊗aspect1. 

	This suggests providing a partial ordering on aspects
giving their priorities and providing axioms that permit deducing
the ordering on ⊗ab from the sentences that describe the ordering
relations.  We haven't been able to work this out yet.  It would
apparently be a considerable elaboration of the formalism.

	I am hopeful that %2prioritized circumscription%1 will
turn out to be the most natural and powerful variant.

.skip 1
Namely we define %2ab_<_ab'%1 by

!!k4:	%2∀ab ab'.ab < ab' ≡ (∀x.(¬ab aspect2 x ∧ ab' aspect2 x)
∨ ((ab aspect2 x ≡ ab' aspect2 x) ∧ ¬ab aspect1 x ∧ ab' aspect1 x))%1.